Lambda the Ultimate

Monads in Ruby, a several-part work in progress, is an attempt to explain and demonstrate monads in Ruby. It looks pretty good so far, although I feel like we could coax a friendlier syntax out of Ruby with a little effort. Maybe in Part 4!

Obligatory LtU connection: the author credits Dave Herman's Schemer's Introduction to Monads as an inspiration.

(One of my co-workers mentioned this to me. I think he might have been making fun of me...)

FORTRAN 25th anniversary film, 1982, 12.5 minutes. Computer History Museum lot number X2843.2005, donated by Daniel N. Leeson. Windows Media Video (12.8 megabytes)

Another great resource from Paul McJones.

The video quality isn't great, but this is still very much worth your time. It's interesting to see the faces behind the history of our discipline.

I am not going to list all the ideas from the film that are worth discussing. Let me just note that several remarks at the begining show just how remarkable the notion of a programming language really is (or was, at the time).

The guys discussing Fortress will also find several of the comments made in the film interesting.

What kind of task is Ragel good for?

• Lexing programming languages.
• Parsing file formats.
• Creating robust custom protocols.
• Checking your "Theory of Computation" homework.

Features

• Describe arbitrary state machines using regular language operators and/or state tables.
• NFA to DFA conversion.
• Hopcroft's state minimization.
• Embed any number of actions into machines at arbitrary places.
• Control non-determinism using priorities on transitions.
• Visualize output with Graphviz.
• Use byte, double byte or word sized alphabets.
• Generate C/C++/Objective-C code with no dependencies.
• Choose from table or control flow driven output.

My talk will instead present a novel approach to the first-year programming curriculum. Specifically, I will explain how a functional semester ideally prepares students for the true essence of object-oriented programming according to Alan Kay: the systematic construction of small modules of code and the construction of programs without assignment statements. Experience shows that these courses prepare students better for upper-level courses than a year of plain object-oriented programming. Initial reports from our students' co-op employers appear to confirm the experiences of our upper-level instructors. (full abstract)

We discussed this approach (FP as an introduction to OOP) before. This presentation is from FPDE 2005.

Chris Adamson at OnJava.com published interviews with a few language luminaries and Java developers. Inspired by Bruce Tate's book Beyond Java, Adamson argues that Ruby is poised to become Java's successor:

Bruce Tate's Beyond Java argues that Java's reign as the top enterprise development language must eventually come to an end and that, for the first time in a decade, major enterprise innovation is occurring outside of the Java realm. In the book, he looks at the unique traits that has allowed to Java to achieve its unprecedented level of success, and then considers what new languages would have to do and be to succeed Java.

Later chapters look at specific languages contending in this space, and clearly favors Ruby as the front-runner. This comes from Tate's own performance breakthroughs (fueled by Ruby on Rails), an analysis of the language, and anecdotal evidence from others who've tried the language.

Is Ruby already shaping up to succeed Java? What's broken with Java that Ruby fixes? And are the two mutually incompatible?

To survey the situation, we contacted several prominent authors, bloggers, and developers to get their takes. Their responses are reprinted in whole in this article.

The interviews are a very interesting read, and the dialogue covers a diverse range of topics. The power of Ruby on Rails is a common theme throughout, and Tate argues that Rails is the catalyst that will push Ruby into the mainstream. What I don't understand is this: if Rails will make Ruby the next Java, why didn't Zope do that for Python?

X10 is a type-safe, modern, parallel, distributed object-oriented language intended to be very easily accessible to Java(TM) programmers. It is targeted to future low-end and high-end systems with nodes that are built out of multi-core SMP chips with non-uniform memory hierarchies, and interconnected in scalable cluster configurations. A member of the Partitioned Global Address Space (PGAS) family of languages, X10 highlights the explicit reification of locality in the form of places; lightweight activities embodied in async, future, foreach, and ateach constructs; constructs for termination detection (finish) and phased computation (clocks); the use of lock-free synchronization (atomic blocks); and the manipulation of global arrays and data structures.

X10 was mentioned here a couple of times, but I don't think it was ever discussed at length.

Here's the (relatively empty) IBM Research X10 home page.

There's a neat thread about strong normalization happening on The Types Forum.

If you've ever wondered Why is it useful to have {type systems,reductions,operations,...} that always terminate? this may Illuminate you.
Here are some snippets to give you a feel for the discussion:

I think it is clearer to split Gérard's original question in two:

1. Is strong normalization useful for programming languages ?
2. Is the proof of strong normalization via type systems applicable for programming languages?

-- François-Régis Sinot

Termination is good:

If a program is a solution to a problem then knowing that it terminates
for any input is an important aspect of it being a solution. Often the
best way to see that it is terminating is expressing it in a language
where all programs terminate. The programming language Epigram is an
example of an experimental language which is intended to be terminating
(even though not all conditions are enforced in the current version), see
http://www.e-pig.org/ for more information.

-- Thorsten Altenkirch

Termination is good!

I think the moral sense of strong normalization is that a program
in a strictly-typed language can only diverge as a result of some
programming construct, which _explicitly_ permits looping, like
iteration, recursion etc. My favourite example here is that the
"big Omega" can be written in Algol 60, because procedure types
in this language are not fully specified.

-- Pawel Urzyczyn

Termination is good and with fixpoints is turing complete?

Another way to put this is that data structures should be definable in a
strongly-normalising language so that data access, etc. is guaranteed to
terminate. Then add fixpoints or loops to describe arbitrary computations.

-- Barry Jay

Terminating reductions allows exhaustive applications of optimizations:

In a compiler, if a set of reductions is strongly normalizing, then the compiler can apply them exhaustively to an intermediate-language term without fear of looping. (We rely on this in the MLj and SML.NET compilers' "simplify" compilation phases, which apply simple reductions and directed commuting conversions until a normal form is reached. Though it has to be said that it's not the classical SN results that are relevant here, but something more specific to our intermediate language and the simplifying reductions that we employ).

-- Andrew Kenney

Rene Vestergaard also gave a link to a 2004 discussion of strong normalization on the rewriting list.

Extensible Records With Scoped Labels
Daan Leijen

Records provide a safe and flexible way to construct data structures. We describe a natural approach to typing polymorphic and extensible records that is simple, easy to use in practice, and straightforward to implement. A novel aspect of this work is that records can contain duplicate labels, effectively introducing a form of scoping over the labels. Furthermore, it is a fully orthogonal extension to existing type systems and programming languages...

Last time one of Daan's papers was mentioned, there was a very positive response (after Frank reminded us a couple of times). This is equally good: clever, elegant, and clearly presented.

(Between this and the Sheard paper, it's a good week for practical type systems...)

via LtU forums:

Putting Curry-Howard to Work

The Curry-Howard isomorphism states that types are propositions and that programs are proofs. This allows programmers to state and enforce invariants of programs by using types. Unfortunately, the type systems of today's functional languages cannot directly express interesting properties of programs. To alleviate this problem, we propose the addition of three new features to functional programming languages such as Haskell: Generalized Algebraic Datatypes, Extensible Kind Systems, and the generation, propagation, and discharging of Static Propositions. These three new features are backward compatible with existing features, and combine to enable a new programming paradigm for functional programmers. This paradigm makes it possible to state and enforce interesting properties of programs using the type system, and it does this in manner that leaves intact the functional programming style, known and loved by functional programmers everywhere.

The paper is short and reasonably easy to read, also the examples are very realistic - check section 13 as a starter.

Getting half through the paper made we willing to play with implementation, getting to the last page made my hands itching to implement my own PL with a similar type system.

You are warned :)

The most recent version of Objective Caml is 3.09.0. It was released on 2005-10-27.

Some of the highlights in release 3.09 are:

• Introduction of private row types, for abstracting the row variable in object and variant types.
• Added warnings Y and Z for local variables that are bound but never used.
• More portable implementation of the -pack option to ocamlopt.

For more information, please consult the comprehensive list of changes.